The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^2)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

K tuples:none
Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(3) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))

We considered the (Usable) Rules:

Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)

And the Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x₁, x₂)) = [1] + [2]x₁   
POL(Case(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(Concat(x₁, x₂)) = [2] + [2]x₁ + [4]x₂   
POL(Cons_sum(x₁, x₂, x₃)) = [2] + x₃   
POL(Cons_usual(x₁, x₂, x₃)) = x₂ + x₃   
POL(FROZEN(x₁, x₂, x₃, x₄)) = x₁ + x₃   
POL(Frozen(x₁, x₂, x₃, x₄)) = [4] + [2]x₁ + [3]x₃ + [3]x₄   
POL(Id) = [5]   
POL(Left) = [5]   
POL(Right) = [3]   
POL(SUM_SUB(x₁, x₂)) = x₁   
POL(Sum_constant(x₁)) = [3]   
POL(Sum_sub(x₁, x₂)) = [3]x₁   
POL(Sum_term_var(x₁)) = 0   
POL(TERM_SUB(x₁, x₂)) = x₁   
POL(Term_app(x₁, x₂)) = [2] + x₁ + x₂   
POL(Term_inl(x₁)) = x₁   
POL(Term_inr(x₁)) = [5] + x₁   
POL(Term_pair(x₁, x₂)) = [3] + x₁ + x₂   
POL(Term_sub(x₁, x₂)) = [2] + x₁ + [2]x₂   
POL(Term_var(x₁)) = [2]   
POL(c(x₁, x₂)) = x₁ + x₂   
POL(c1(x₁, x₂)) = x₁ + x₂   
POL(c10(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c16(x₁)) = x₁   
POL(c17(x₁, x₂)) = x₁ + x₂   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c19(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(c9(x₁, x₂)) = x₁ + x₂   

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

K tuples:

TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))

Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(5) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))

We considered the (Usable) Rules:

Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)

And the Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x₁, x₂)) = [2] + [2]x₁   
POL(Case(x₁, x₂, x₃)) = [2] + x₁ + x₃   
POL(Concat(x₁, x₂)) = [1] + [4]x₁ + [4]x₂   
POL(Cons_sum(x₁, x₂, x₃)) = x₃   
POL(Cons_usual(x₁, x₂, x₃)) = [2] + x₂ + x₃   
POL(FROZEN(x₁, x₂, x₃, x₄)) = x₁ + x₃   
POL(Frozen(x₁, x₂, x₃, x₄)) = [4] + [2]x₁ + [2]x₂ + [3]x₃ + [4]x₄   
POL(Id) = [5]   
POL(Left) = [3]   
POL(Right) = [2]   
POL(SUM_SUB(x₁, x₂)) = 0   
POL(Sum_constant(x₁)) = 0   
POL(Sum_sub(x₁, x₂)) = [3]x₁   
POL(Sum_term_var(x₁)) = [3]   
POL(TERM_SUB(x₁, x₂)) = x₁   
POL(Term_app(x₁, x₂)) = [3] + x₁ + x₂   
POL(Term_inl(x₁)) = [2] + x₁   
POL(Term_inr(x₁)) = x₁   
POL(Term_pair(x₁, x₂)) = x₁ + x₂   
POL(Term_sub(x₁, x₂)) = [4] + [2]x₁ + [2]x₂   
POL(Term_var(x₁)) = [5]   
POL(c(x₁, x₂)) = x₁ + x₂   
POL(c1(x₁, x₂)) = x₁ + x₂   
POL(c10(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c16(x₁)) = x₁   
POL(c17(x₁, x₂)) = x₁ + x₂   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c19(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(c9(x₁, x₂)) = x₁ + x₂   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

K tuples:

TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))

Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(7) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

K tuples:

TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))

Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

We considered the (Usable) Rules:

Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)

And the Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x₁, x₂)) = [3] + [4]x₁   
POL(Case(x₁, x₂, x₃)) = [2] + x₁ + x₂ + x₃   
POL(Concat(x₁, x₂)) = [4] + x₁ + [4]x₂   
POL(Cons_sum(x₁, x₂, x₃)) = [1] + x₃   
POL(Cons_usual(x₁, x₂, x₃)) = [1] + x₂ + x₃   
POL(FROZEN(x₁, x₂, x₃, x₄)) = [3] + [2]x₁ + [2]x₃   
POL(Frozen(x₁, x₂, x₃, x₄)) = [3] + [2]x₁ + [4]x₂ + [5]x₃ + [5]x₄   
POL(Id) = [3]   
POL(Left) = [3]   
POL(Right) = [3]   
POL(SUM_SUB(x₁, x₂)) = [1] + x₁   
POL(Sum_constant(x₁)) = [3]   
POL(Sum_sub(x₁, x₂)) = [3] + [3]x₁ + [3]x₂   
POL(Sum_term_var(x₁)) = [2]   
POL(TERM_SUB(x₁, x₂)) = [2]x₁   
POL(Term_app(x₁, x₂)) = x₁ + x₂   
POL(Term_inl(x₁)) = x₁   
POL(Term_inr(x₁)) = x₁   
POL(Term_pair(x₁, x₂)) = x₁ + x₂   
POL(Term_sub(x₁, x₂)) = [4] + x₁ + [4]x₂   
POL(Term_var(x₁)) = [2]   
POL(c(x₁, x₂)) = x₁ + x₂   
POL(c1(x₁, x₂)) = x₁ + x₂   
POL(c10(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c16(x₁)) = x₁   
POL(c17(x₁, x₂)) = x₁ + x₂   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c19(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(c9(x₁, x₂)) = x₁ + x₂   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))

K tuples:

TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))

We considered the (Usable) Rules:

Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)

And the Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x₁, x₂)) = [2] + [5]x₁   
POL(Case(x₁, x₂, x₃)) = [5] + x₁ + x₂ + x₃   
POL(Concat(x₁, x₂)) = [5] + [4]x₁ + [2]x₂   
POL(Cons_sum(x₁, x₂, x₃)) = [3] + x₃   
POL(Cons_usual(x₁, x₂, x₃)) = [1] + x₂ + x₃   
POL(FROZEN(x₁, x₂, x₃, x₄)) = [5] + [4]x₁ + [4]x₂ + [4]x₃   
POL(Frozen(x₁, x₂, x₃, x₄)) = [2] + [2]x₁ + [4]x₂ + [2]x₃   
POL(Id) = [5]   
POL(Left) = [5]   
POL(Right) = [2]   
POL(SUM_SUB(x₁, x₂)) = [3] + [2]x₁   
POL(Sum_constant(x₁)) = [3]   
POL(Sum_sub(x₁, x₂)) = [4]   
POL(Sum_term_var(x₁)) = [3]   
POL(TERM_SUB(x₁, x₂)) = [4] + [4]x₁   
POL(Term_app(x₁, x₂)) = [4] + x₁ + x₂   
POL(Term_inl(x₁)) = [4] + x₁   
POL(Term_inr(x₁)) = [4] + x₁   
POL(Term_pair(x₁, x₂)) = [2] + x₁ + x₂   
POL(Term_sub(x₁, x₂)) = [2] + x₁ + [2]x₂   
POL(Term_var(x₁)) = [4]   
POL(c(x₁, x₂)) = x₁ + x₂   
POL(c1(x₁, x₂)) = x₁ + x₂   
POL(c10(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c16(x₁)) = x₁   
POL(c17(x₁, x₂)) = x₁ + x₂   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c19(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(c9(x₁, x₂)) = x₁ + x₂   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))

K tuples:

TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))

Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))

We considered the (Usable) Rules:

Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)

And the Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x₁, x₂)) = [3] + [5]x₁   
POL(Case(x₁, x₂, x₃)) = [1] + x₁ + x₂ + x₃   
POL(Concat(x₁, x₂)) = [2] + [5]x₁ + [4]x₂   
POL(Cons_sum(x₁, x₂, x₃)) = [3] + x₃   
POL(Cons_usual(x₁, x₂, x₃)) = x₂ + x₃   
POL(FROZEN(x₁, x₂, x₃, x₄)) = [1] + [2]x₁ + [2]x₃   
POL(Frozen(x₁, x₂, x₃, x₄)) = [3] + [2]x₁ + [4]x₂ + [3]x₃ + [3]x₄   
POL(Id) = [2]   
POL(Left) = [3]   
POL(Right) = [5]   
POL(SUM_SUB(x₁, x₂)) = [2]x₁   
POL(Sum_constant(x₁)) = [3]   
POL(Sum_sub(x₁, x₂)) = [2] + [5]x₁ + [3]x₂   
POL(Sum_term_var(x₁)) = [2]   
POL(TERM_SUB(x₁, x₂)) = [2]x₁   
POL(Term_app(x₁, x₂)) = x₁ + x₂   
POL(Term_inl(x₁)) = [1] + x₁   
POL(Term_inr(x₁)) = [2] + x₁   
POL(Term_pair(x₁, x₂)) = [2] + x₁ + x₂   
POL(Term_sub(x₁, x₂)) = [4] + x₁ + [4]x₂   
POL(Term_var(x₁)) = [2]   
POL(c(x₁, x₂)) = x₁ + x₂   
POL(c1(x₁, x₂)) = x₁ + x₂   
POL(c10(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c16(x₁)) = x₁   
POL(c17(x₁, x₂)) = x₁ + x₂   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c19(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(c9(x₁, x₂)) = x₁ + x₂   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))

K tuples:

TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))

Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))

We considered the (Usable) Rules:

Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)

And the Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x₁, x₂)) = [5] + [4]x₁   
POL(Case(x₁, x₂, x₃)) = [4] + x₁ + x₂ + x₃   
POL(Concat(x₁, x₂)) = [3] + [4]x₁ + [4]x₂   
POL(Cons_sum(x₁, x₂, x₃)) = [4] + x₃   
POL(Cons_usual(x₁, x₂, x₃)) = [4] + x₂ + x₃   
POL(FROZEN(x₁, x₂, x₃, x₄)) = [4] + [4]x₁ + [4]x₃   
POL(Frozen(x₁, x₂, x₃, x₄)) = [5] + [3]x₁ + [2]x₂ + [3]x₃ + [4]x₄   
POL(Id) = [5]   
POL(Left) = [4]   
POL(Right) = [2]   
POL(SUM_SUB(x₁, x₂)) = [2]x₁   
POL(Sum_constant(x₁)) = [3]   
POL(Sum_sub(x₁, x₂)) = [4] + [4]x₁ + [4]x₂   
POL(Sum_term_var(x₁)) = [4]   
POL(TERM_SUB(x₁, x₂)) = [1] + [4]x₁   
POL(Term_app(x₁, x₂)) = [4] + x₁ + x₂   
POL(Term_inl(x₁)) = [4] + x₁   
POL(Term_inr(x₁)) = [3] + x₁   
POL(Term_pair(x₁, x₂)) = [2] + x₁ + x₂   
POL(Term_sub(x₁, x₂)) = [4] + [4]x₁ + x₂   
POL(Term_var(x₁)) = [2]   
POL(c(x₁, x₂)) = x₁ + x₂   
POL(c1(x₁, x₂)) = x₁ + x₂   
POL(c10(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c16(x₁)) = x₁   
POL(c17(x₁, x₂)) = x₁ + x₂   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c19(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(c9(x₁, x₂)) = x₁ + x₂   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:

TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))

K tuples:

TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))

Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(17) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))

We considered the (Usable) Rules:

Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)

And the Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x₁, x₂)) = [2] + [2]x₁   
POL(Case(x₁, x₂, x₃)) = [1] + x₁ + x₃   
POL(Concat(x₁, x₂)) = [3] + x₁ + x₂   
POL(Cons_sum(x₁, x₂, x₃)) = [5] + x₃   
POL(Cons_usual(x₁, x₂, x₃)) = [4] + x₂ + x₃   
POL(FROZEN(x₁, x₂, x₃, x₄)) = x₁ + x₃   
POL(Frozen(x₁, x₂, x₃, x₄)) = [2] + [3]x₁ + [3]x₂ + [5]x₃ + [3]x₄   
POL(Id) = [2]   
POL(Left) = [3]   
POL(Right) = [3]   
POL(SUM_SUB(x₁, x₂)) = 0   
POL(Sum_constant(x₁)) = [2]   
POL(Sum_sub(x₁, x₂)) = [5]x₁ + [2]x₂   
POL(Sum_term_var(x₁)) = 0   
POL(TERM_SUB(x₁, x₂)) = x₁   
POL(Term_app(x₁, x₂)) = x₁ + x₂   
POL(Term_inl(x₁)) = [5] + x₁   
POL(Term_inr(x₁)) = [5] + x₁   
POL(Term_pair(x₁, x₂)) = [3] + x₁ + x₂   
POL(Term_sub(x₁, x₂)) = [2] + [2]x₁ + [2]x₂   
POL(Term_var(x₁)) = [4]   
POL(c(x₁, x₂)) = x₁ + x₂   
POL(c1(x₁, x₂)) = x₁ + x₂   
POL(c10(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c16(x₁)) = x₁   
POL(c17(x₁, x₂)) = x₁ + x₂   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c19(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(c9(x₁, x₂)) = x₁ + x₂   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:

TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))

K tuples:

TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))

Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(19) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))

We considered the (Usable) Rules:

Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)

And the Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x₁, x₂)) = x₁·x₂ + [2]x₁²   
POL(Case(x₁, x₂, x₃)) = [3] + x₁ + x₃   
POL(Concat(x₁, x₂)) = [2]x₁ + x₂ + x₁·x₂   
POL(Cons_sum(x₁, x₂, x₃)) = [1] + x₁ + x₂ + x₃   
POL(Cons_usual(x₁, x₂, x₃)) = [1] + x₁ + x₂ + x₃   
POL(FROZEN(x₁, x₂, x₃, x₄)) = [2]x₁ + [2]x₃ + x₄ + x₃·x₄ + x₁·x₄ + [2]x₁² + x₁·x₃ + [2]x₃² + x₂²   
POL(Frozen(x₁, x₂, x₃, x₄)) = [3] + [2]x₁ + [2]x₃ + [3]x₄ + x₃·x₄ + x₂·x₄ + x₁·x₄   
POL(Id) = 0   
POL(Left) = 0   
POL(Right) = 0   
POL(SUM_SUB(x₁, x₂)) = [1] + [2]x₂   
POL(Sum_constant(x₁)) = 0   
POL(Sum_sub(x₁, x₂)) = [1]   
POL(Sum_term_var(x₁)) = 0   
POL(TERM_SUB(x₁, x₂)) = x₁·x₂ + [2]x₁²   
POL(Term_app(x₁, x₂)) = [1] + x₁ + x₂   
POL(Term_inl(x₁)) = x₁   
POL(Term_inr(x₁)) = x₁   
POL(Term_pair(x₁, x₂)) = [3] + x₁ + x₂   
POL(Term_sub(x₁, x₂)) = [2]x₁ + x₂ + x₁·x₂   
POL(Term_var(x₁)) = [1]   
POL(c(x₁, x₂)) = x₁ + x₂   
POL(c1(x₁, x₂)) = x₁ + x₂   
POL(c10(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c16(x₁)) = x₁   
POL(c17(x₁, x₂)) = x₁ + x₂   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c19(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(c9(x₁, x₂)) = x₁ + x₂   

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:

TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))

K tuples:

TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))

Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(21) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))

We considered the (Usable) Rules:

Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)

And the Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x₁, x₂)) = [2]x₁ + [2]x₁·x₂ + x₁²   
POL(Case(x₁, x₂, x₃)) = [1] + x₁ + x₃   
POL(Concat(x₁, x₂)) = x₁ + x₂ + [2]x₁·x₂   
POL(Cons_sum(x₁, x₂, x₃)) = [2] + x₃   
POL(Cons_usual(x₁, x₂, x₃)) = [1] + x₂ + x₃   
POL(FROZEN(x₁, x₂, x₃, x₄)) = [1] + [3]x₁ + [3]x₃ + [2]x₃·x₄ + [2]x₁·x₄ + x₁² + x₃²   
POL(Frozen(x₁, x₂, x₃, x₄)) = [1] + x₁ + x₃ + [2]x₄ + [2]x₃·x₄ + [2]x₁·x₄   
POL(Id) = 0   
POL(Left) = 0   
POL(Right) = 0   
POL(SUM_SUB(x₁, x₂)) = [2]   
POL(Sum_constant(x₁)) = 0   
POL(Sum_sub(x₁, x₂)) = 0   
POL(Sum_term_var(x₁)) = 0   
POL(TERM_SUB(x₁, x₂)) = [2]x₁ + [2]x₁·x₂ + x₁²   
POL(Term_app(x₁, x₂)) = [2] + x₁ + x₂   
POL(Term_inl(x₁)) = x₁   
POL(Term_inr(x₁)) = x₁   
POL(Term_pair(x₁, x₂)) = [1] + x₁ + x₂   
POL(Term_sub(x₁, x₂)) = x₁ + x₂ + [2]x₁·x₂   
POL(Term_var(x₁)) = [2]   
POL(c(x₁, x₂)) = x₁ + x₂   
POL(c1(x₁, x₂)) = x₁ + x₂   
POL(c10(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c16(x₁)) = x₁   
POL(c17(x₁, x₂)) = x₁ + x₂   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c19(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(c9(x₁, x₂)) = x₁ + x₂   

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:

SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))

K tuples:

TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))

Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(23) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))

We considered the (Usable) Rules:

Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)

And the Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x₁, x₂)) = x₁·x₂ + x₁²   
POL(Case(x₁, x₂, x₃)) = [1] + x₁ + x₃   
POL(Concat(x₁, x₂)) = x₁ + x₂ + x₁·x₂ + x₁²   
POL(Cons_sum(x₁, x₂, x₃)) = x₃   
POL(Cons_usual(x₁, x₂, x₃)) = [1] + x₂ + x₃   
POL(FROZEN(x₁, x₂, x₃, x₄)) = x₃·x₄ + x₁·x₄ + x₁² + x₃²   
POL(Frozen(x₁, x₂, x₃, x₄)) = [1] + [2]x₁ + x₃ + [2]x₄ + x₃·x₄ + x₁·x₄ + x₁² + [2]x₁·x₃ + x₃²   
POL(Id) = 0   
POL(Left) = 0   
POL(Right) = 0   
POL(SUM_SUB(x₁, x₂)) = [1] + x₂   
POL(Sum_constant(x₁)) = 0   
POL(Sum_sub(x₁, x₂)) = 0   
POL(Sum_term_var(x₁)) = 0   
POL(TERM_SUB(x₁, x₂)) = x₁·x₂ + x₁²   
POL(Term_app(x₁, x₂)) = [2] + x₁ + x₂   
POL(Term_inl(x₁)) = [1] + x₁   
POL(Term_inr(x₁)) = x₁   
POL(Term_pair(x₁, x₂)) = [1] + x₁ + x₂   
POL(Term_sub(x₁, x₂)) = x₁ + x₂ + x₁·x₂ + x₁²   
POL(Term_var(x₁)) = 0   
POL(c(x₁, x₂)) = x₁ + x₂   
POL(c1(x₁, x₂)) = x₁ + x₂   
POL(c10(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c16(x₁)) = x₁   
POL(c17(x₁, x₂)) = x₁ + x₂   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c19(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(c9(x₁, x₂)) = x₁ + x₂   

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:

SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))

K tuples:

TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))

Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(25) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))

We considered the (Usable) Rules:

Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)

And the Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x₁, x₂)) = x₁ + x₁·x₂   
POL(Case(x₁, x₂, x₃)) = [2] + x₁ + x₃   
POL(Concat(x₁, x₂)) = [2]x₁ + x₂ + [2]x₁·x₂   
POL(Cons_sum(x₁, x₂, x₃)) = [2] + x₃   
POL(Cons_usual(x₁, x₂, x₃)) = [2] + x₂ + x₃   
POL(FROZEN(x₁, x₂, x₃, x₄)) = x₁ + x₃ + x₃·x₄ + x₁·x₄   
POL(Frozen(x₁, x₂, x₃, x₄)) = [2] + [2]x₁ + [2]x₃ + [2]x₄ + [2]x₃·x₄ + [2]x₁·x₄   
POL(Id) = 0   
POL(Left) = 0   
POL(Right) = 0   
POL(SUM_SUB(x₁, x₂)) = [2]x₂   
POL(Sum_constant(x₁)) = 0   
POL(Sum_sub(x₁, x₂)) = 0   
POL(Sum_term_var(x₁)) = 0   
POL(TERM_SUB(x₁, x₂)) = x₁ + x₁·x₂   
POL(Term_app(x₁, x₂)) = [2] + x₁ + x₂   
POL(Term_inl(x₁)) = [2] + x₁   
POL(Term_inr(x₁)) = [2] + x₁   
POL(Term_pair(x₁, x₂)) = [2] + x₁ + x₂   
POL(Term_sub(x₁, x₂)) = [2]x₁ + x₂ + [2]x₁·x₂   
POL(Term_var(x₁)) = x₁   
POL(c(x₁, x₂)) = x₁ + x₂   
POL(c1(x₁, x₂)) = x₁ + x₂   
POL(c10(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c16(x₁)) = x₁   
POL(c17(x₁, x₂)) = x₁ + x₂   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c19(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(c9(x₁, x₂)) = x₁ + x₂   

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:none
K tuples:

TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))

Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(27) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(28) BOUNDS(O(1), O(1))